package systemfnomabss

/**
   * adapted from parser for untyped lambda calculus by Miles Sabin 
   */

trait AbstractSyntax  extends systemfnomabss.syntax.Binding with systemfnomabss.syntax.BindingSyntax{ self : AbstractSyntax => 

sealed trait Node

type Term = LTerm
type Type = LType
sealed abstract class LTerm extends Nominal[LTerm] with Node
sealed trait BaseValue extends LTerm {
  def baseType: LType
  //val name: String
  //def swap(a: Name, b: Name): Self
  def fresh(a: Name)=true
  def supp: List[Name]=Nil
  def swap(a: Name, b: Name) = this
  //def subst(sub: Name => Option[LTerm]): AM[LTerm] = AM.result(this)
}




      case class Tru extends LTerm with BaseValue{
        override def toString = "true"
        override def baseType = TyBool()
      }
      case class Fls extends LTerm with BaseValue{
        override def toString= "false"
        override def baseType = TyBool()
      }
      case class Unit extends LTerm with BaseValue{
        override def toString = "unit"
        override def baseType = TyUnit()
      }
      case class Lit(n: int) extends LTerm with BaseValue{
        override def toString = n.toString
        override def baseType = TyInt()
      }
      
case class If(cond: LTerm, pos: LTerm, neg: LTerm) extends LTerm {
  def swap(a: Name, b: Name) = If(cond swap(a, b), pos swap(a, b), neg swap(a, b))
  def fresh(a: Name) = (cond fresh a) && (pos fresh a) && (neg fresh a)
  def supp = (cond supp) ::: (pos supp) ::: (neg supp)
}

case class Var(n: Name) extends LTerm {
  def swap(a: Name, b: Name) = Var(n swap(a, b))    
  def fresh(a: Name) = n fresh(a)
  def supp = n supp

}

case class App(fun: LTerm, arg: LTerm) extends LTerm {
  def swap(a: Name, b: Name) = App(fun swap(a, b), arg swap(a, b))
  def fresh(a: Name) = fun.fresh(a) && arg.fresh(a)
  def supp = fun.supp ::: arg.supp

}

case class Lam(ty:LType, abs: \\[LTerm]) extends LTerm {
  def swap(a: Name, b: Name) = Lam(ty swap(a,b),abs swap(a, b))
  def fresh(a: Name) = (ty fresh(a)) && (abs fresh(a))
  def supp = ty.supp  ::: abs.supp

}

//ackward, TODO: generalized binders like in nameplate paper to create a fitting type of abstraction for this
case class Let(t1: LTerm, abs: \\[LTerm]) extends LTerm {
  def swap(a: Name, b: Name) = Let(t1 swap (a,b), abs swap(a,b))
  def fresh(a: Name) = (t1 fresh(a)) && (abs fresh(a))
  def supp = t1.supp ::: abs.supp
}

case class TLam(abs: \\[LTerm]) extends LTerm {
  def swap(a: Name, b: Name) = TLam(abs swap(a, b))
  def fresh(a: Name) = abs fresh(a)
  def supp = abs supp
}
  

case class TApp(t:LTerm, ty: LType) extends LTerm {
  def swap(a: Name, b: Name) = TApp(t swap(a, b), ty swap(a, b))
  def fresh(a: Name) = t.fresh(a) && ty.fresh(a)
  def supp = t.supp ::: ty.supp
}

case class Pack(ty:LType, t:LTerm, pubty:LType) extends LTerm {
  def swap(a:Name, b:Name) = Pack(ty swap(a,b), t swap(a,b), pubty swap(a,b) )
  def fresh(a: Name) = ty.fresh(a) && t.fresh(a) && pubty.fresh(a)
  def supp = ty.supp ::: t.supp ::: pubty.supp
}

//composition of body should be: tyvar\\Lam(tyvar, termvar\\body)
case class Unpack(impl: LTerm, pubty_pubvar_body: \\[LTerm]) extends LTerm {
  def swap(a:Name, b:Name) = Unpack(impl swap(a,b), pubty_pubvar_body swap(a,b))
  def fresh(a:Name) = impl.fresh(a) && pubty_pubvar_body.fresh(a)
  def supp = impl.supp ::: pubty_pubvar_body.supp
}

case class RecProj(t: LTerm, label: String) extends LTerm {
  def swap(a:Name, b:Name) = RecProj(t swap(a,b), label)
  def fresh(a:Name) = t.fresh(a)
  def supp = t.supp
}
case class Record(fields: List[(String,LTerm)]) extends LTerm {
  override def toString = "{" + fields.foldRight("")({case ((s,t),xs) => s +"="+ t +", "+ xs} )+ "}"
  def fieldsmap[R](f:LTerm=>R):List[(String,R)] =
    fields.map({case (label,fld)=> (label,f(fld))})
  def field(label:String) = {
      val results = fields.filter( {case (fldlabel,fldtype) => label == fldlabel}).map(_ _2)
      if (results.length == 0)throw new TypeExc("no label "+label+" in record")
      if (results.length >1  )throw new TypeExc("multiple labels "+label+" in record")
      results.head
  }
    
  def swap(a:Name, b:Name) = Record (
                              for { (label, content) <- fields}
                              yield (label, content.swap(a,b))
                              )
  def fresh(a:Name) = fields.map( {case (n,c)=> c.fresh(a)}).forall( _ == true)                 
  def supp =  fields.flatMap( {case (a,b)=>  b.supp})  
}














sealed abstract class LType extends Nominal[LType] with Node


sealed trait BaseType extends LType {
  val name: String
  //def swap(a: Name, b: Name): Self
  def fresh(a: Name)=true
  def supp: List[Name]=Nil
  def swap(a: Name, b: Name) = this
  def subst(sub: Name => Option[LType]): LType = this
}
case class TyBool() extends LType with BaseType
{ val name="Bool" }
case class TyInt()  extends LType with BaseType
{ val name="Int"  }
case class TyUnit() extends LType with BaseType
{ val name="Unit" }

case class TyVar(n: Name) extends LType 
{ 
  def swap(a: Name, b: Name)= TyVar(n swap(a,b))
  def fresh(a: Name)= n fresh a
  def supp: List[Name]= n supp
  
  def subst(sub: Name => Option[LType]) : LType = sub(n).getOrElse[LType](this)
}
case class TyArr(t1: LType, t2: LType) extends LType {
  def swap(a: Name, b: Name)= TyArr(t1 swap(a,b), t2 swap(a,b))
  def fresh(a: Name)= (t1 fresh a) && (t2 fresh a)
  def supp: List[Name]= (t1 supp) ::: (t2 supp) 
  /*
  def subst(sub: Name => Option[LType]) : LType = 
  { val t1b = t1 subst sub;
    val t2b = t2 subst sub;
    TyArr(t1b,t2b) }
    */

}
case class TyUniv(abs: \\[LType]) extends LType  {
  def swap(a: Name, b: Name) = TyUniv(abs swap(a,b))
  def fresh(a: Name) = abs fresh(a)
  def supp = abs supp
  /*
  def subst(sub: Name => Option[LType]): LType = {
      val abs2 = new AbsSubstTo[LType].AbsIsSubstable(abs) subst(sub);
      TyUniv( abs2) }
      */
}
case class TyExist(abs: \\[LType]) extends LType {
  def swap(a: Name, b: Name) = TyExist(abs swap(a,b))
  def fresh(a: Name) = abs fresh(a)
  def supp = abs supp
  
  /*
  def subst(sub: Name => Option[LType]): LType = {
      val abs2 = new AbsSubstTo[LType].AbsIsSubstable(abs) subst(sub);
      TyExist( abs2) }
      */
}
case class TyRecord(fields: List[(String,LType)]) extends LType {
  def map[R](f:LType=>R):List[(String,R)] =
      fields.map({case (label,fld)=> (label,f(fld))})
  def field(label:String) = {
      val results = fields.filter( {case (fldlabel,fldtype) => label == fldlabel}).map(_ _2)
      if (results.length == 0)throw new TypeExc("no label "+label+" in record")
      if (results.length >1  )throw new TypeExc("multiple labels "+label+" in record")
      results.head
  }
  def swap(a:Name, b:Name) = TyRecord (
                              for { (label, content) <- fields}
                              yield (label, content.swap(a,b))
                              )
  def fresh(a:Name) = fields.map( {case (n,c)=> (c.fresh(a))}).forall( _ == true)                 
  def supp =  fields.flatMap( {case (a,b)=> b.supp})

}














 /*
 type VarRef = Int
 type VarHint = String
 
 

   sealed trait LTerm 

trait BaseValue extends LTerm {
  def baseType():BaseType
}


 case class Tru extends LTerm with BaseValue{
   override def toString = "true"
   override def baseType = TyBool
 }
 case class Fls extends LTerm with BaseValue{
   override def toString= "false"
   override def baseType = TyBool
 }
 case class Unit extends LTerm with BaseValue{
   override def toString = "unit"
   override def baseType = TyUnit
 }
 case class Lit(n: int) extends LTerm with BaseValue{
   override def toString = n.toString
   override def baseType = TyInt
 }
 
 
 case class If(cond: LTerm, pos: LTerm, neg: LTerm) extends LTerm {

 }

 
 

 case class Var(n: VarRef) extends LTerm  {
 }
 
 case class Lam(hint: VarHint, ty: LType, body: LTerm) extends LTerm {
 }
 
 case class App(funt:LTerm, argt:LTerm) extends LTerm {
 }
 
 //TVar -> see TyVar
 case class TLam(hint: VarHint, t:LTerm) extends LTerm {
 }
 case class TApp(t1:LTerm, ty: LType) extends LTerm {
 }
 
 case class Pack(ty:LType, t:LTerm, pubty:LType) extends LTerm {
 }
 
 case class Unpack(impl: LTerm, pubty:String,pubvar:String, body:LTerm) extends LTerm {
 }
 
 
 
 
 case class Let(n: VarHint, t1: LTerm, t2: LTerm) extends LTerm {
   override def toString = "let "+n+" = "+t1+" in "+t2
 }
 
 
 case class Record(fields: List[(String,LTerm)]) extends LTerm {
   override def toString = "{" + fields.foldRight("")({case ((s,t),xs) => s +"="+ t +", "+ xs} )+ "}"
   def fieldsmap[R](f:LTerm=>R):List[(String,R)] =
     fields.map({case (label,fld)=> (label,f(fld))})
 }
 case class RecProj(t: LTerm, label: String) extends LTerm {
   
 }



 sealed trait LType extends LTerm 
 
 trait BaseType extends LType {
   val name: String
   override def toString = name
 }
 
 case class TyBool() extends LType with BaseType
 { val name="Bool" }
 case class TyInt()  extends LType with BaseType
 { val name="Int"  }
 case class TyTop()  extends LType with BaseType
 { val name="Top"  }
 case class TyUnit() extends LType with BaseType
 { val name="Unit" }

 
 case class TyVar(n: VarRef) extends LType {
 }
 case class TyArr(fundom: LType, funrange: LType) extends LType {
   if (null==fundom || null==funrange) throw new NullPointerException()
   override def toString = "("+fundom +" => " +funrange+")"
   def map(f:LType=>LType):TyArr=
      TyArr(f(fundom), f(funrange))
 }

 case class TyUniv(x: VarHint, ty: LType) extends LType  {
   override def toString = "forall "+x +". "+ty
   override def equals(o: Any) = o match {
     case TyUniv(ox,oty) => ty == oty
     case _ => false
 }
 }
 case class TyExist(x:String, ty: LType) extends LType {
   override def toString = "{forsome "+x+","+ty+"}"
   override def equals(o: Any) = o match {
     case TyExist(ox,oty) => ty == oty
     case _ => false
   }}

 case class TyRecord(fields: List[(String,LType)]) extends LType {
   def map[R](f:LType=>R):List[(String,R)] =
       fields.map({case (label,fld)=> (label,f(fld))})
   def field(label:String) = {
       val results = fields.filter( {case (fldlabel,fldtype) => label == fldlabel}).map(_ _2)
       if (results.length == 0)throw new TypeExc("no label "+label+" in record")
       if (results.length >1  )throw new TypeExc("multiple labels "+label+" in record")
       results.head
   }
 }
 
 */


}
 

